//  /=============================================================/
//  |   Auteurs  : J.JULLIEN / R.HERLEMAN / R.CHAILAN             |
//  |   Fichier  : clause.h                                       |
//  |   Date     : 12/04/2009                                     |
//  |   Objet    : Spécification du type "t_Clause" &             |
//  |              ses fonctions associées                        |
//  /=============================================================/

#include <stdio.h>
#include <stdlib.h>

#include "litteral.h"

/* ------------------------------------------------------------------------ */
/* ---------------------- Déclaration types exportés ---------------------- */
/* ------------------------------------------------------------------------ */

typedef enum { SATISFAITE, FALSIFIEE, INCHANGEE, RACCOURCIE } t_Etat;

typedef struct t_Clause {
  int numClause;
  t_Etat etat;
  t_Litteral *litteral;
  t_Litteral *dernierLitteral;  // Pointeur de queue de la liste chaînée de
                                // littéraux, pour insertion en fin
  
  int nbVariables;
  int nbNeutres;
  int nbFalsifies;
  int nbSatisfaits;
  
  struct t_Clause* hashSuiv;    // Pointeur sur la clause précédente dans la
                                // liste doublement chaînée de la table de
                                // hashage
  struct t_Clause* hashPred;    // Pointeur sur la clause suivante dans la
                                // liste doublement chaînée de la table de
                                // hashage
} t_Clause;

/* ------------------------------------------------------------------------ */
/* -------------------- Déclaration fonctions exportés -------------------- */
/* ------------------------------------------------------------------------ */

/*----------------------------------------------------------------------------
Nom              : clauseInit
Prérequis        : num est bien un numéro de clause existant
Action           : Initialisation de tous les champs d'une clause et
                   retourne la clause initialisée à un etat "INCHANGEE" et son
                   numéro numClause initialisé à num
Type de retour   : t_Clause
Variable(s)      :  
  E   int   num - Numéro de la clause
----------------------------------------------------------------------------*/
t_Clause clauseInit (int num);

/*----------------------------------------------------------------------------
Nom              : clauseMAJCompteurs
Prérequis        : c != NULL
Action           : Met à jour les compteurs et l'état de la clause c
Type de retour   : -
Variable(s)      :  
  E/S t_Clause*    c - La clause qui doit être mise à jour
  E   t_Litteral   l - Un littéral afin de connaître la valeur du littéral
  E   int          ancienneVal - Ancienne valeur de la variable 1 ou 0 sinon
                   neutre
  E   int          nouvelleVal - Nouvelle valeur de la variable 1 ou 0 sinon
                   neutre
----------------------------------------------------------------------------*/
void clauseMAJCompteurs (t_Clause* c, t_Litteral l, int ancienneVal,
                         int nouvelleVal);
                         
/*----------------------------------------------------------------------------
Nom              : clauseEstVide
Prérequis        : -
Action           : Retourne vrai si la clause c n'a pas de litteral, faux
                   sinon
Type de retour   : int
Variable(s)      :  
  E t_Clause   c - La clause à tester
----------------------------------------------------------------------------*/
int clauseEstVide (t_Clause c);

/*----------------------------------------------------------------------------
Nom              : clauseAjouterLitteral
Prérequis        : lit != NULL
Action           : Ajoute le litteral lit en fin de la liste des litteraux de
                   la clause c
Type de retour   : -
Variable(s)      :  
  E/S t_Clause     c - La clause dans laquelle il faut ajouter lit
  E   t_Litteral   lit - Le littéral à ajouter
----------------------------------------------------------------------------*/
void clauseAjouterLitteral (t_Clause* c, t_Litteral* lit);

/*----------------------------------------------------------------------------
Nom              : clauseGetLitteral
Prérequis        : -
Action           : Retourne un pointeur sur le premier littéral de la clause
                   (null s'il n'y en a pas)
Type de retour   : t_Litteral*
Variable(s)      :  
  E t_Clause   c - La clause dont on veut le littéral
----------------------------------------------------------------------------*/
t_Litteral* clauseGetLitteral (t_Clause c);

/*----------------------------------------------------------------------------
Nom              : clauseAfficherLigne
Prérequis        : -
Action           : Affiche la clause sous forme de ligne pour l'affichage au
                   sein de d'un tableau
Type de retour   : -
Variable(s)      :
  E   t_Clause   clause - Clauses à afficher
----------------------------------------------------------------------------*/
void clauseAfficherLigne (t_Clause clause);

/*----------------------------------------------------------------------------
Nom              : clauseAfficherEnsemble
Prérequis        : -
Action           : Affiche la clause sous forme d'ensemble de litteraux
Type de retour   : -
Variable(s)      :
  E   t_Clause   clause - Clauses à afficher
----------------------------------------------------------------------------*/
void clauseAfficherEnsemble (t_Clause clause);

/*----------------------------------------------------------------------------
Nom              : clauseAfficherFormule
Prérequis        : -
Action           : Affiche la clause sous forme de formule logique
                   (disjonction de litteraux)
Type de retour   : -
Variable(s)      :
  E   t_Clause   clause - Clauses à afficher
----------------------------------------------------------------------------*/
void clauseAfficherFormule (t_Clause clause);

/*----------------------------------------------------------------------------
Nom              : clauseAfficherDebug
Prérequis        : -
Action           : Affiche des informations détaillées sur la clause
Type de retour   : -
Variable(s)      :
  E   t_Clause   c - Clauses à afficher
----------------------------------------------------------------------------*/
void clauseAfficherDebug (t_Clause c);
